Languages, specifications. So how do we know if a program is correct? Any program without

a specification is by definition correct because you don't know what it's doing. So you need

to know the intent of a program before you can say that it is correct. You need to have

some way of specifying what the intent of a program is. And that requires a specification.

So now we need to ensure, to allow a program to be proven correct, you need a specification

and an implementation. So how do we specify such a specification for a programming language?

That's the topic of today. So the ideas here are, for example, model-based development.

A model is sort of an abstract implementation, and then you have the actual implementation

somewhere in the background. So for example, you have some sort of domain-specific language

for some problem domain, and then you have a C, C++ implementation somewhere else. What

is currently state of the art is programming something in a model, and then leave some

black boxes in the model for the actual implementation so the implementation can be generated from

the model. Instead of having a completely separate model and a completely separate implementation,

you somehow try and push everything into this model. Another way is doing sort of refinement-based

development of your application. So you start with a simple prototype with lots of details

left out, and then you slowly refine that prototype to get an implementation. This prototype

that you started out with is effectively the model. So with prototype-based languages,

you usually create a sort of skeleton, and then you refine that skeleton by gluing things

on the skeleton until the program has the functionality that you required. So the general

idea in either way is to have two languages, one language for specifying stuff, what the

intent of a program is, and another language for doing the implementation. And the differences

in between these approaches is in how close these two languages are, how closely are they

integrated. Right, so how does a specification then communicate its intent with the implementation?

Somehow, you need to be able to map the implementation with the specification. So you need to have

some way of mapping these two languages together. So for example, you can do this via variables.

So we have a model of your application, and there you have a variable number or temperature,

and in your implementation, you have the same variable, temperature. And you have a mapping

saying that this temperature variable there is the same variable intended in the implementation,

also called temperature. And so you have some sort of mapping between variables in implementation

and model, and then you can say that this should be the same as that over there. Right,

so the hope is that the specification can then be automatically verified because it's

a very high level, so it's a specification. It leaves out all the details that make automatic

verification theorem proving hard to do. So a model is simple and therefore verifiable.

You cannot automatically verify, for example, some low level C code. That is almost impossible

to do. But if you leave out all the details, then the program becomes so small that it

is verifiable again. So COG, for example, is a language for proving things correct.

It's a proof assistant. It is not really a proof checker. It's a proof assistant. So

you write your theorems, your axioms, your facts inside of this COG language, and then

you say, COG, please prove it to me. Prove that it is consistent with each other or internally

consistent. And then COG will try and apply rules and theorems to see if it can be proven.

If not, then it asks the programmer of this COG language to give it more facts to be able

to continue proving things. So ideally in COG, you have a large library of ways of proving

things, and you invoke that library to prove your specification correct or internally consistent.

A little bit about COG. So you have propositions, you have sets, mathematical sets, and you

have abstract data types. An abstract data type is just an ADT as we know it, as we've

seen it before, where you cannot look into the internals of an ADT. So tau over e is

in the type of some expression. So tau of 3 is an integer. It's a type of, as we saw

it before. So tau of e is true or false if something is inside of that category, inside

of a member of that type. So with check e, we can then ask the type of an expression.

So if you say, what is the type of some addition, then that's that value, and that is a natural